This tutorial assumes you know how to construct LC instances; if not, see the tutorial on Constructing LCs. This tutorial covers what it means for a symbol to be free or bound inside an LC tree.

(Each piece of sample code below is written as if it were a script sitting in the root folder of this source code repository, and run from there with the command-line tools node. If you place your scripts in another folder, you will need to adjust the path in each import statement accordingly. If you have not yet set up a copy of this repository with the appropriate Node.js version installed, see our GitHub README, which explains how to do so.)

Free variables vs. free symbols

Most situations that deal with the concepts of free/bound with respect to binding expressions speak of free and bound variables. But in the world of LCs, we do not have variables as a specific category; we have only the general category of symbols that can be used as variables or constants. Thus here we will speak of free and bound symbols.

The concept of a bound variable has the usual meaning: Inside any Binding expression (head sym1 sym2 ... symN , body), the symbols sym1 through symN are bound. Outside of that expression (assuming there is no containing binding expression of the same symbol(s)), they are not bound, and are thus called free.

import { LogicConcept } from './src/index.js'

const binding = LogicConcept.fromPutdown( '(forall x , (P x))' )[0]
binding.descendantsSatisfying( d => d.isAtomic() ).map( d => {
    console.log( 'Is', d.toPutdown(), 'free?', d.isFree() )
} )

// Console output:
Is forall free? true
Is x free? false
Is P free? true
Is x free? false

You can also ask the question relatively: Is a symbol free in a specific ancestor?

const outerBinding = LogicConcept.fromPutdown( '(exists x , (forall y , (> x y)))' )[0]
const innerBinding = outerBinding.body()
const secondX = innerBinding.body().child( 1 )
console.log( 'Is x free in the inner binding?', secondX.isFree( innerBinding ) )
console.log( 'Is x free in the outer binding?', secondX.isFree( outerBinding ) )

// Console output:
file:///Users/monks/Dropbox/files/monkware/git/lde/tutorial-tmp-file-Free%20and%20bound%20variables.md.js:9
const innerBinding = outerBinding.body()
                                  ^

TypeError: outerBinding.body is not a function
    at file:///Users/monks/Dropbox/files/monkware/git/lde/tutorial-tmp-file-Free%20and%20bound%20variables.md.js:9:35
    at ModuleJob.run (node:internal/modules/esm/module_job:198:25)
    at async Promise.all (index 0)
    at async ESMLoader.import (node:internal/modules/esm/loader:409:24)
    at async loadESM (node:internal/process/esm_loader:85:5)
    at async handleMainPromise (node:internal/modules/run_main:61:12)

Node.js v18.4.0

The isFree() method works not only for symbols. You can ask whether a nonatomic expression is free, and it will be free if and only if all of the symbols free within it are free in the given context.

console.log( innerBinding.body().isFree( innerBinding ) )

Free occurrences

We can also ask whether a symbol occurs free anywhere in an expression. Note the difference between x.occursFree(y) and y.occursFree(x) and that the order may be different from what you expect.

import { LurchSymbol } from './src/index.js'

const example = LogicConcept.fromPutdown( '(and (> x 1) (forall x , (R x x)))' )[0]
console.log( 'Last x free?', example.child( 2 ).body().child( 2 ).isFree() )
console.log( 'Any x free?', example.occursFree( new LurchSymbol( 'x' ) ) )

You can get all free occurrences by combining descendantsSatisfying() with isFree().

Variable capture and replacing free occurrences

The usual notion of variable capture exists when considering substitution into a binding, and you can check to see if it will happen using isFreeToReplace(). You can do all of the free replacements with replaceFree().

console.log( 'Before:', example.toPutdown() )
example.replaceFree(
    new LurchSymbol( 'x' ),
    LogicConcept.fromPutdown( '(- 3 x)' )[0] )
console.log( 'After:', example.toPutdown() )